Continuing with #1167, this moves all the stuff about separation axioms into a separate file. I included a few other things that aren't explicitly "T0-T6", but felt comfortable here, such as zero-dimensional and perfect sets.

There are still some critical results about separation axioms (AKA urysohn's lemma and friends) that are trapped in normedtype.v due to some boring facts about the reals. We need to build the edist function for a pseudoMetric, which requires a few small things about R. Some results generalize to any orderTopologicalType such as \min is continuous. Others can live in ereal.v. It'll take some effort to break that stuff up, though. So I'll leave it for a later PR.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels